Inference at * 
Iof proof for Lemma p-mu wf:


  P:(), x:( + Top). p-mu(P;x)   

latex

 by (Unfold `p-mu` ( 0)) 
CollapseTHEN (Auto) 

latex

C.

Definitions	p-mu(P;x), , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), #$n, {i..j}, {x:A| B(x)} , i  j < k, P & Q, A  B, A, b, x:A. B(x), f(a), left + right, Type, Top, x:AB(x), , t  T,
Lemmas	int seg wf, le wf, not wf, assert wf, top wf, nat wf, bool wf